Problem: a__g(X) -> a__h(X) a__c() -> d() a__h(d()) -> a__g(c()) mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) mark(c()) -> a__c() mark(d()) -> d() a__g(X) -> g(X) a__h(X) -> h(X) a__c() -> c() Proof: Bounds Processor: bound: 3 enrichment: match automaton: final states: {8,7,6,5} transitions: c1() -> 29* h1(65) -> 66* h1(79) -> 80* h1(71) -> 72* h1(73) -> 74* g1(55) -> 56* g1(57) -> 58* g1(49) -> 50* g1(63) -> 64* d1() -> 25* a__c1() -> 47* a__h1(15) -> 16* a__h1(17) -> 18* a__h1(9) -> 10* a__h1(23) -> 24* a__g1(45) -> 46* a__g1(37) -> 38* a__g1(39) -> 40* a__g1(29) -> 30* a__g1(31) -> 32* c2() -> 139* h2(137) -> 138* h2(129) -> 130* h2(131) -> 132* h2(123) -> 124* a__g0(2) -> 5* a__g0(4) -> 5* a__g0(1) -> 5* a__g0(3) -> 5* g2(107) -> 108* g2(121) -> 122* g2(113) -> 114* g2(115) -> 116* g2(105) -> 106* a__h0(2) -> 7* a__h0(4) -> 7* a__h0(1) -> 7* a__h0(3) -> 7* d2() -> 101* a__c0() -> 6* a__h2(85) -> 86* a__h2(99) -> 100* a__h2(91) -> 92* a__h2(93) -> 94* a__h2(83) -> 84* d0() -> 1* h3(147) -> 148* h3(159) -> 160* h3(141) -> 142* h3(153) -> 154* h3(155) -> 156* c0() -> 2* mark0(2) -> 8* mark0(4) -> 8* mark0(1) -> 8* mark0(3) -> 8* g0(2) -> 3* g0(4) -> 3* g0(1) -> 3* g0(3) -> 3* h0(2) -> 4* h0(4) -> 4* h0(1) -> 4* h0(3) -> 4* 1 -> 71,55,39,15 2 -> 79,63,31,23 3 -> 65,49,45,9 4 -> 73,57,37,17 9 -> 131* 10 -> 8,5 15 -> 137* 16 -> 8,5 17 -> 123* 18 -> 8,5 23 -> 129* 24 -> 8,5 25 -> 8,6 29 -> 107,85,6 30 -> 94,40,16,5,8,7 31 -> 113,91 32 -> 8* 37 -> 105,83 38 -> 8* 39 -> 115,93 40 -> 8* 45 -> 121,99 46 -> 8* 47 -> 8* 50 -> 5* 56 -> 5* 58 -> 5* 64 -> 5* 66 -> 7* 72 -> 7* 74 -> 7* 80 -> 7* 83 -> 159* 84 -> 38* 85 -> 141* 86 -> 30* 91 -> 153* 92 -> 32* 93 -> 155* 94 -> 40,8 99 -> 147* 100 -> 46,8 101 -> 47,8 106 -> 38* 108 -> 30* 114 -> 32* 116 -> 40,8 122 -> 46,8 124 -> 18* 130 -> 24* 132 -> 10,8,5 138 -> 16,8,5 139 -> 47,8 142 -> 86,30,16 148 -> 100,46 154 -> 92,32 156 -> 94,40 160 -> 84,38 problem: Qed